(set-info :smt-lib-version 2.6)
(set-logic QF_NRA)
(set-info :source |Benchmarks generated from hycomp (https://es-static.fbk.eu/tools/hycomp/). BMC instances of non-linear hybrid automata taken from: Alessandro Cimatti, Sergio Mover, Stefano Tonetta, A quantifier-free SMT encoding of non-linear hybrid automata, FMCAD 2012 and Alessandro Cimatti, Sergio Mover, Stefano Tonetta, Quantier-free encoding of invariants for Hybrid Systems, Formal Methods in System Design. This instance solves a BMC problem of depth 2 and uses the quantifier free encoding with lemmas encoding. Contacts: Sergio Mover (mover@fbk.eu), Stefano Tonetta (tonettas@fbk.eu), Alessandro Cimatti (cimatti@fbk.eu).|)
(set-info :category "industrial")
(set-info :status unsat)
;; MathSAT API call trace
;; generated on Mon Mar 19 10:38:46 2012
(declare-fun m.event_is_timed__AT0 () Bool)
(declare-fun m.time__AT2 () Real)
(declare-fun m.y__AT2 () Real)
(declare-fun m.x__AT1 () Real)
(declare-fun m.delta__AT2 () Real)
(declare-fun m.x__AT2 () Real)
(declare-fun m.EVENT.0__AT2 () Bool)
(declare-fun m.EVENT.1__AT2 () Bool)
(declare-fun m.delta__AT0 () Real)
(declare-fun m.time__AT1 () Real)
(declare-fun m.speed_y__AT0 () Real)
(declare-fun m.EVENT.0__AT0 () Bool)
(declare-fun m.delta__AT1 () Real)
(declare-fun m.EVENT.1__AT0 () Bool)
(declare-fun m.y__AT1 () Real)
(declare-fun m.speed_x__AT2 () Real)
(declare-fun m.speed_y__AT2 () Real)
(declare-fun m.event_is_timed__AT1 () Bool)
(declare-fun m.y__AT0 () Real)
(declare-fun m.speed_x__AT1 () Real)
(declare-fun m.speed_y__AT1 () Real)
(declare-fun m.time__AT0 () Real)
(declare-fun m.x__AT0 () Real)
(declare-fun m.EVENT.0__AT1 () Bool)
(declare-fun m.event_is_timed__AT2 () Bool)
(declare-fun m.EVENT.1__AT1 () Bool)
(declare-fun m.speed_x__AT0 () Real)
(assert (let ((.def_1428 (* m.speed_y__AT2 m.delta__AT2)))
(let ((.def_1429 (* 10.0 .def_1428)))
(let ((.def_1101 (* m.delta__AT2 m.delta__AT2)))
(let ((.def_1427 (* (- 49.0) .def_1101)))
(let ((.def_1430 (+ .def_1427 .def_1429)))
(let ((.def_1431 (* 10.0 m.y__AT2)))
(let ((.def_1433 (+ .def_1431 .def_1430)))
(let ((.def_1458 (<= .def_1433 0.0 )))
(let ((.def_1466 (not .def_1458)))
(let ((.def_1456 (<= m.y__AT2 0.0 )))
(let ((.def_1467 (or .def_1456 .def_1466)))
(let ((.def_1062 (<= 0.0 m.y__AT2)))
(let ((.def_1464 (not .def_1062)))
(let ((.def_1454 (<= 0.0 .def_1433)))
(let ((.def_1465 (or .def_1454 .def_1464)))
(let ((.def_1468 (and .def_1465 .def_1467)))
(let ((.def_1269 (<= m.speed_y__AT2 0.0 )))
(let ((.def_1270 (not .def_1269)))
(let ((.def_1263 (* (- 49.0) m.delta__AT2)))
(let ((.def_1264 (* 5.0 m.speed_y__AT2)))
(let ((.def_1266 (+ .def_1264 .def_1263)))
(let ((.def_1267 (<= .def_1266 0.0 )))
(let ((.def_1268 (not .def_1267)))
(let ((.def_1271 (or .def_1268 .def_1270)))
(let ((.def_1272 (not .def_1271)))
(let ((.def_1469 (or .def_1272 .def_1468)))
(let ((.def_1460 (not .def_1454)))
(let ((.def_1461 (or .def_1062 .def_1460)))
(let ((.def_1457 (not .def_1456)))
(let ((.def_1459 (or .def_1457 .def_1458)))
(let ((.def_1462 (and .def_1459 .def_1461)))
(let ((.def_1279 (<= 0.0 .def_1266)))
(let ((.def_1280 (not .def_1279)))
(let ((.def_1277 (<= 0.0 m.speed_y__AT2)))
(let ((.def_1278 (not .def_1277)))
(let ((.def_1281 (or .def_1278 .def_1280)))
(let ((.def_1282 (not .def_1281)))
(let ((.def_1463 (or .def_1282 .def_1462)))
(let ((.def_1470 (and .def_1463 .def_1469)))
(let ((.def_1455 (and .def_1062 .def_1454)))
(let ((.def_1471 (and .def_1455 .def_1470)))
(let ((.def_1291 (and .def_1267 .def_1269)))
(let ((.def_1288 (or .def_1277 .def_1280)))
(let ((.def_1287 (or .def_1267 .def_1270)))
(let ((.def_1289 (and .def_1287 .def_1288)))
(let ((.def_1292 (and .def_1289 .def_1291)))
(let ((.def_1286 (and .def_1277 .def_1279)))
(let ((.def_1290 (and .def_1286 .def_1289)))
(let ((.def_1293 (or .def_1290 .def_1292)))
(let ((.def_1472 (and .def_1293 .def_1471)))
(let ((.def_1434 (<= .def_1433 1000.0 )))
(let ((.def_1446 (not .def_1434)))
(let ((.def_1061 (<= m.y__AT2 100.0 )))
(let ((.def_1447 (or .def_1061 .def_1446)))
(let ((.def_1440 (<= 100.0 m.y__AT2)))
(let ((.def_1444 (not .def_1440)))
(let ((.def_1438 (<= 1000.0 .def_1433)))
(let ((.def_1445 (or .def_1438 .def_1444)))
(let ((.def_1448 (and .def_1445 .def_1447)))
(let ((.def_1449 (or .def_1272 .def_1448)))
(let ((.def_1439 (not .def_1438)))
(let ((.def_1441 (or .def_1439 .def_1440)))
(let ((.def_1436 (not .def_1061)))
(let ((.def_1437 (or .def_1434 .def_1436)))
(let ((.def_1442 (and .def_1437 .def_1441)))
(let ((.def_1443 (or .def_1282 .def_1442)))
(let ((.def_1450 (and .def_1443 .def_1449)))
(let ((.def_1435 (and .def_1061 .def_1434)))
(let ((.def_1451 (and .def_1435 .def_1450)))
(let ((.def_1452 (and .def_1293 .def_1451)))
(let ((.def_1105 (* (- (/ 49 10)) m.speed_y__AT2)))
(let ((.def_1151 (* 3.0 .def_1105)))
(let ((.def_1324 (* (- 1.0) .def_1151)))
(let ((.def_1352 (* 2.0 .def_1324)))
(let ((.def_1396 (* (- 1.0) .def_1352)))
(let ((.def_1397 (* m.delta__AT2 .def_1396)))
(let ((.def_1398 (* (- 50.0) .def_1397)))
(let ((.def_1121 (* m.speed_x__AT2 m.speed_x__AT2)))
(let ((.def_1221 (* (- 50.0) .def_1121)))
(let ((.def_1403 (+ .def_1221 .def_1398)))
(let ((.def_1109 (* m.speed_y__AT2 m.speed_y__AT2)))
(let ((.def_1219 (* (- 50.0) .def_1109)))
(let ((.def_1404 (+ .def_1219 .def_1403)))
(let ((.def_1223 (* (- 7203.0) .def_1101)))
(let ((.def_1405 (+ .def_1223 .def_1404)))
(let ((.def_1225 (* 490.0 m.y__AT2)))
(let ((.def_1406 (+ .def_1225 .def_1405)))
(let ((.def_1409 (<= 0.0 .def_1406)))
(let ((.def_1416 (not .def_1409)))
(let ((.def_1234 (* (- 5.0) .def_1121)))
(let ((.def_1233 (* (- 5.0) .def_1109)))
(let ((.def_1235 (+ .def_1233 .def_1234)))
(let ((.def_1236 (* 49.0 m.y__AT2)))
(let ((.def_1238 (+ .def_1236 .def_1235)))
(let ((.def_1249 (<= 0.0 .def_1238)))
(let ((.def_1417 (or .def_1249 .def_1416)))
(let ((.def_1407 (<= .def_1406 0.0 )))
(let ((.def_1239 (<= .def_1238 0.0 )))
(let ((.def_1240 (not .def_1239)))
(let ((.def_1415 (or .def_1240 .def_1407)))
(let ((.def_1418 (and .def_1415 .def_1417)))
(let ((.def_1419 (or .def_1282 .def_1418)))
(let ((.def_1411 (not .def_1407)))
(let ((.def_1412 (or .def_1239 .def_1411)))
(let ((.def_1250 (not .def_1249)))
(let ((.def_1410 (or .def_1250 .def_1409)))
(let ((.def_1413 (and .def_1410 .def_1412)))
(let ((.def_1414 (or .def_1272 .def_1413)))
(let ((.def_1420 (and .def_1414 .def_1419)))
(let ((.def_1408 (and .def_1239 .def_1407)))
(let ((.def_1421 (and .def_1408 .def_1420)))
(let ((.def_1422 (and .def_1293 .def_1421)))
(let ((.def_1353 (* m.delta__AT2 .def_1352)))
(let ((.def_1354 (* 50.0 .def_1353)))
(let ((.def_1359 (+ .def_1221 .def_1354)))
(let ((.def_1360 (+ .def_1219 .def_1359)))
(let ((.def_1361 (+ .def_1223 .def_1360)))
(let ((.def_1362 (+ .def_1225 .def_1361)))
(let ((.def_1373 (<= .def_1362 0.0 )))
(let ((.def_1374 (not .def_1373)))
(let ((.def_1390 (or .def_1239 .def_1374)))
(let ((.def_1363 (<= 0.0 .def_1362)))
(let ((.def_1389 (or .def_1250 .def_1363)))
(let ((.def_1391 (and .def_1389 .def_1390)))
(let ((.def_1392 (or .def_1272 .def_1391)))
(let ((.def_1364 (not .def_1363)))
(let ((.def_1386 (or .def_1249 .def_1364)))
(let ((.def_1385 (or .def_1240 .def_1373)))
(let ((.def_1387 (and .def_1385 .def_1386)))
(let ((.def_1388 (or .def_1282 .def_1387)))
(let ((.def_1393 (and .def_1388 .def_1392)))
(let ((.def_1384 (and .def_1249 .def_1363)))
(let ((.def_1394 (and .def_1384 .def_1393)))
(let ((.def_1395 (and .def_1293 .def_1394)))
(let ((.def_1423 (or .def_1395 .def_1422)))
(let ((.def_1162 (* 2.0 .def_1121)))
(let ((.def_1336 (* (- 1.0) .def_1162)))
(let ((.def_1337 (* m.delta__AT2 .def_1336)))
(let ((.def_1338 (* 25.0 .def_1337)))
(let ((.def_1113 (* (- (/ 49 10)) m.y__AT2)))
(let ((.def_1158 (* 2.0 .def_1113)))
(let ((.def_1332 (* (- 1.0) .def_1158)))
(let ((.def_1333 (* m.delta__AT2 .def_1332)))
(let ((.def_1334 (* 50.0 .def_1333)))
(let ((.def_1343 (+ .def_1334 .def_1338)))
(let ((.def_1154 (* 2.0 .def_1109)))
(let ((.def_1328 (* (- 1.0) .def_1154)))
(let ((.def_1329 (* m.delta__AT2 .def_1328)))
(let ((.def_1330 (* 25.0 .def_1329)))
(let ((.def_1344 (+ .def_1330 .def_1343)))
(let ((.def_1325 (* .def_1101 .def_1324)))
(let ((.def_1326 (* 50.0 .def_1325)))
(let ((.def_1345 (+ .def_1326 .def_1344)))
(let ((.def_1125 (* m.x__AT2 m.speed_x__AT2)))
(let ((.def_1170 (* (- 50.0) .def_1125)))
(let ((.def_1346 (+ .def_1170 .def_1345)))
(let ((.def_1117 (* m.y__AT2 m.speed_y__AT2)))
(let ((.def_1168 (* (- 50.0) .def_1117)))
(let ((.def_1347 (+ .def_1168 .def_1346)))
(let ((.def_1102 (* m.delta__AT2 .def_1101)))
(let ((.def_1166 (* (- 2401.0) .def_1102)))
(let ((.def_1348 (+ .def_1166 .def_1347)))
(let ((.def_1172 (* 1000.0 m.speed_x__AT2)))
(let ((.def_1349 (+ .def_1172 .def_1348)))
(let ((.def_1367 (<= .def_1349 0.0 )))
(let ((.def_1378 (not .def_1367)))
(let ((.def_1184 (* (- 1.0) .def_1125)))
(let ((.def_1183 (* (- 1.0) .def_1117)))
(let ((.def_1185 (+ .def_1183 .def_1184)))
(let ((.def_1186 (* 20.0 m.speed_x__AT2)))
(let ((.def_1188 (+ .def_1186 .def_1185)))
(let ((.def_1189 (<= .def_1188 0.0 )))
(let ((.def_1379 (or .def_1189 .def_1378)))
(let ((.def_1350 (<= 0.0 .def_1349)))
(let ((.def_1203 (<= 0.0 .def_1188)))
(let ((.def_1204 (not .def_1203)))
(let ((.def_1377 (or .def_1204 .def_1350)))
(let ((.def_1380 (and .def_1377 .def_1379)))
(let ((.def_1375 (or .def_1240 .def_1374)))
(let ((.def_1376 (not .def_1375)))
(let ((.def_1381 (or .def_1376 .def_1380)))
(let ((.def_1369 (not .def_1350)))
(let ((.def_1370 (or .def_1203 .def_1369)))
(let ((.def_1190 (not .def_1189)))
(let ((.def_1368 (or .def_1190 .def_1367)))
(let ((.def_1371 (and .def_1368 .def_1370)))
(let ((.def_1365 (or .def_1250 .def_1364)))
(let ((.def_1366 (not .def_1365)))
(let ((.def_1372 (or .def_1366 .def_1371)))
(let ((.def_1382 (and .def_1372 .def_1381)))
(let ((.def_1351 (and .def_1203 .def_1350)))
(let ((.def_1383 (and .def_1351 .def_1382)))
(let ((.def_1424 (and .def_1383 .def_1423)))
(let ((.def_1216 (* 2.0 .def_1151)))
(let ((.def_1295 (* (- 1.0) .def_1216)))
(let ((.def_1296 (* m.delta__AT2 .def_1295)))
(let ((.def_1297 (* 50.0 .def_1296)))
(let ((.def_1302 (+ .def_1221 .def_1297)))
(let ((.def_1303 (+ .def_1219 .def_1302)))
(let ((.def_1304 (+ .def_1223 .def_1303)))
(let ((.def_1305 (+ .def_1225 .def_1304)))
(let ((.def_1308 (<= .def_1305 0.0 )))
(let ((.def_1315 (not .def_1308)))
(let ((.def_1316 (or .def_1239 .def_1315)))
(let ((.def_1306 (<= 0.0 .def_1305)))
(let ((.def_1314 (or .def_1250 .def_1306)))
(let ((.def_1317 (and .def_1314 .def_1316)))
(let ((.def_1318 (or .def_1272 .def_1317)))
(let ((.def_1310 (not .def_1306)))
(let ((.def_1311 (or .def_1249 .def_1310)))
(let ((.def_1309 (or .def_1240 .def_1308)))
(let ((.def_1312 (and .def_1309 .def_1311)))
(let ((.def_1313 (or .def_1282 .def_1312)))
(let ((.def_1319 (and .def_1313 .def_1318)))
(let ((.def_1307 (and .def_1249 .def_1306)))
(let ((.def_1320 (and .def_1307 .def_1319)))
(let ((.def_1321 (and .def_1293 .def_1320)))
(let ((.def_1217 (* m.delta__AT2 .def_1216)))
(let ((.def_1218 (* (- 50.0) .def_1217)))
(let ((.def_1227 (+ .def_1221 .def_1218)))
(let ((.def_1228 (+ .def_1219 .def_1227)))
(let ((.def_1229 (+ .def_1223 .def_1228)))
(let ((.def_1230 (+ .def_1225 .def_1229)))
(let ((.def_1247 (<= 0.0 .def_1230)))
(let ((.def_1248 (not .def_1247)))
(let ((.def_1275 (or .def_1248 .def_1249)))
(let ((.def_1231 (<= .def_1230 0.0 )))
(let ((.def_1274 (or .def_1231 .def_1240)))
(let ((.def_1276 (and .def_1274 .def_1275)))
(let ((.def_1283 (or .def_1276 .def_1282)))
(let ((.def_1232 (not .def_1231)))
(let ((.def_1261 (or .def_1232 .def_1239)))
(let ((.def_1260 (or .def_1247 .def_1250)))
(let ((.def_1262 (and .def_1260 .def_1261)))
(let ((.def_1273 (or .def_1262 .def_1272)))
(let ((.def_1284 (and .def_1273 .def_1283)))
(let ((.def_1259 (and .def_1231 .def_1239)))
(let ((.def_1285 (and .def_1259 .def_1284)))
(let ((.def_1294 (and .def_1285 .def_1293)))
(let ((.def_1322 (or .def_1294 .def_1321)))
(let ((.def_1163 (* m.delta__AT2 .def_1162)))
(let ((.def_1164 (* (- 25.0) .def_1163)))
(let ((.def_1159 (* m.delta__AT2 .def_1158)))
(let ((.def_1160 (* (- 50.0) .def_1159)))
(let ((.def_1174 (+ .def_1160 .def_1164)))
(let ((.def_1155 (* m.delta__AT2 .def_1154)))
(let ((.def_1156 (* (- 25.0) .def_1155)))
(let ((.def_1175 (+ .def_1156 .def_1174)))
(let ((.def_1152 (* .def_1101 .def_1151)))
(let ((.def_1153 (* (- 50.0) .def_1152)))
(let ((.def_1176 (+ .def_1153 .def_1175)))
(let ((.def_1177 (+ .def_1170 .def_1176)))
(let ((.def_1178 (+ .def_1168 .def_1177)))
(let ((.def_1179 (+ .def_1166 .def_1178)))
(let ((.def_1180 (+ .def_1172 .def_1179)))
(let ((.def_1201 (<= 0.0 .def_1180)))
(let ((.def_1202 (not .def_1201)))
(let ((.def_1254 (or .def_1202 .def_1203)))
(let ((.def_1181 (<= .def_1180 0.0 )))
(let ((.def_1253 (or .def_1181 .def_1190)))
(let ((.def_1255 (and .def_1253 .def_1254)))
(let ((.def_1251 (or .def_1248 .def_1250)))
(let ((.def_1252 (not .def_1251)))
(let ((.def_1256 (or .def_1252 .def_1255)))
(let ((.def_1182 (not .def_1181)))
(let ((.def_1244 (or .def_1182 .def_1189)))
(let ((.def_1243 (or .def_1201 .def_1204)))
(let ((.def_1245 (and .def_1243 .def_1244)))
(let ((.def_1241 (or .def_1232 .def_1240)))
(let ((.def_1242 (not .def_1241)))
(let ((.def_1246 (or .def_1242 .def_1245)))
(let ((.def_1257 (and .def_1246 .def_1256)))
(let ((.def_1215 (and .def_1181 .def_1189)))
(let ((.def_1258 (and .def_1215 .def_1257)))
(let ((.def_1323 (and .def_1258 .def_1322)))
(let ((.def_1425 (or .def_1323 .def_1424)))
(let ((.def_1129 (* (- 20.0) m.speed_x__AT2)))
(let ((.def_1130 (* m.delta__AT2 .def_1129)))
(let ((.def_1131 (* (- 200.0) .def_1130)))
(let ((.def_1126 (* m.delta__AT2 .def_1125)))
(let ((.def_1127 (* (- 200.0) .def_1126)))
(let ((.def_1139 (+ .def_1127 .def_1131)))
(let ((.def_1122 (* .def_1101 .def_1121)))
(let ((.def_1123 (* (- 100.0) .def_1122)))
(let ((.def_1140 (+ .def_1123 .def_1139)))
(let ((.def_1118 (* m.delta__AT2 .def_1117)))
(let ((.def_1119 (* (- 200.0) .def_1118)))
(let ((.def_1141 (+ .def_1119 .def_1140)))
(let ((.def_1114 (* .def_1101 .def_1113)))
(let ((.def_1115 (* (- 200.0) .def_1114)))
(let ((.def_1142 (+ .def_1115 .def_1141)))
(let ((.def_1110 (* .def_1101 .def_1109)))
(let ((.def_1111 (* (- 100.0) .def_1110)))
(let ((.def_1143 (+ .def_1111 .def_1142)))
(let ((.def_1106 (* .def_1102 .def_1105)))
(let ((.def_1107 (* (- 200.0) .def_1106)))
(let ((.def_1144 (+ .def_1107 .def_1143)))
(let ((.def_1103 (* m.delta__AT2 .def_1102)))
(let ((.def_1104 (* (- 2401.0) .def_1103)))
(let ((.def_1145 (+ .def_1104 .def_1144)))
(let ((.def_1094 (* m.x__AT2 m.x__AT2)))
(let ((.def_1135 (* (- 100.0) .def_1094)))
(let ((.def_1146 (+ .def_1135 .def_1145)))
(let ((.def_1056 (* m.y__AT2 m.y__AT2)))
(let ((.def_1133 (* (- 100.0) .def_1056)))
(let ((.def_1147 (+ .def_1133 .def_1146)))
(let ((.def_1137 (* 4000.0 m.x__AT2)))
(let ((.def_1148 (+ .def_1137 .def_1147)))
(let ((.def_1195 (<= 0.0 .def_1148)))
(let ((.def_1209 (not .def_1195)))
(let ((.def_1095 (* (- 1.0) .def_1094)))
(let ((.def_1093 (* (- 1.0) .def_1056)))
(let ((.def_1096 (+ .def_1093 .def_1095)))
(let ((.def_1097 (* 40.0 m.x__AT2)))
(let ((.def_1099 (+ .def_1097 .def_1096)))
(let ((.def_1193 (<= 0.0 .def_1099)))
(let ((.def_1210 (or .def_1193 .def_1209)))
(let ((.def_1100 (<= .def_1099 0.0 )))
(let ((.def_1207 (not .def_1100)))
(let ((.def_1149 (<= .def_1148 0.0 )))
(let ((.def_1208 (or .def_1149 .def_1207)))
(let ((.def_1211 (and .def_1208 .def_1210)))
(let ((.def_1205 (or .def_1202 .def_1204)))
(let ((.def_1206 (not .def_1205)))
(let ((.def_1212 (or .def_1206 .def_1211)))
(let ((.def_1197 (not .def_1149)))
(let ((.def_1198 (or .def_1100 .def_1197)))
(let ((.def_1194 (not .def_1193)))
(let ((.def_1196 (or .def_1194 .def_1195)))
(let ((.def_1199 (and .def_1196 .def_1198)))
(let ((.def_1191 (or .def_1182 .def_1190)))
(let ((.def_1192 (not .def_1191)))
(let ((.def_1200 (or .def_1192 .def_1199)))
(let ((.def_1213 (and .def_1200 .def_1212)))
(let ((.def_1150 (and .def_1100 .def_1149)))
(let ((.def_1214 (and .def_1150 .def_1213)))
(let ((.def_1426 (and .def_1214 .def_1425)))
(let ((.def_1453 (and .def_1426 .def_1452)))
(let ((.def_1473 (and .def_1453 .def_1472)))
(let ((.def_1071 (* m.speed_x__AT2 m.delta__AT2)))
(let ((.def_1072 (+ m.x__AT2 .def_1071)))
(let ((.def_1078 (<= .def_1072 0.0 )))
(let ((.def_1087 (not .def_1078)))
(let ((.def_1076 (<= m.x__AT2 0.0 )))
(let ((.def_1088 (or .def_1076 .def_1087)))
(let ((.def_1059 (<= 0.0 m.x__AT2)))
(let ((.def_1085 (not .def_1059)))
(let ((.def_1073 (<= 0.0 .def_1072)))
(let ((.def_1086 (or .def_1073 .def_1085)))
(let ((.def_1089 (and .def_1086 .def_1088)))
(let ((.def_1084 (<= m.speed_x__AT2 0.0 )))
(let ((.def_1090 (or .def_1084 .def_1089)))
(let ((.def_1080 (not .def_1073)))
(let ((.def_1081 (or .def_1059 .def_1080)))
(let ((.def_1077 (not .def_1076)))
(let ((.def_1079 (or .def_1077 .def_1078)))
(let ((.def_1082 (and .def_1079 .def_1081)))
(let ((.def_1075 (<= 0.0 m.speed_x__AT2)))
(let ((.def_1083 (or .def_1075 .def_1082)))
(let ((.def_1091 (and .def_1083 .def_1090)))
(let ((.def_1074 (and .def_1059 .def_1073)))
(let ((.def_1092 (and .def_1074 .def_1091)))
(let ((.def_1474 (and .def_1092 .def_1473)))
(let ((.def_1067 (<= m.x__AT1 20.0 )))
(let ((.def_1063 (and .def_1061 .def_1062)))
(let ((.def_1054 (+ m.x__AT2 (- 20.0) )))
(let ((.def_1055 (* .def_1054 .def_1054)))
(let ((.def_1057 (+ .def_1055 .def_1056)))
(let ((.def_1058 (<= 400.0 .def_1057)))
(let ((.def_1060 (and .def_1058 .def_1059)))
(let ((.def_1064 (and .def_1060 .def_1063)))
(let ((.def_1052 (not m.EVENT.0__AT2)))
(let ((.def_1050 (not m.EVENT.1__AT2)))
(let ((.def_1053 (or .def_1050 .def_1052)))
(let ((.def_1065 (and .def_1053 .def_1064)))
(let ((.def_1044 (<= 0.0 m.delta__AT1)))
(let ((.def_551 (not m.EVENT.0__AT1)))
(let ((.def_549 (not m.EVENT.1__AT1)))
(let ((.def_975 (and .def_549 .def_551)))
(let ((.def_977 (not .def_975)))
(let ((.def_1045 (or .def_977 .def_1044)))
(let ((.def_1046 (or m.EVENT.1__AT1 .def_1045)))
(let ((.def_1032 (* (- 10.0) m.y__AT2)))
(let ((.def_927 (* m.speed_y__AT1 m.delta__AT1)))
(let ((.def_928 (* 10.0 .def_927)))
(let ((.def_1036 (+ .def_928 .def_1032)))
(let ((.def_600 (* m.delta__AT1 m.delta__AT1)))
(let ((.def_926 (* (- 49.0) .def_600)))
(let ((.def_1037 (+ .def_926 .def_1036)))
(let ((.def_930 (* 10.0 m.y__AT1)))
(let ((.def_1038 (+ .def_930 .def_1037)))
(let ((.def_1039 (= .def_1038 0.0 )))
(let ((.def_1027 (* (- 5.0) m.speed_y__AT2)))
(let ((.def_762 (* (- 49.0) m.delta__AT1)))
(let ((.def_1028 (+ .def_762 .def_1027)))
(let ((.def_763 (* 5.0 m.speed_y__AT1)))
(let ((.def_1029 (+ .def_763 .def_1028)))
(let ((.def_1030 (= .def_1029 0.0 )))
(let ((.def_570 (* m.speed_x__AT1 m.delta__AT1)))
(let ((.def_1022 (* (- 1.0) .def_570)))
(let ((.def_521 (* (- 1.0) m.x__AT1)))
(let ((.def_1023 (+ .def_521 .def_1022)))
(let ((.def_1024 (+ m.x__AT2 .def_1023)))
(let ((.def_1025 (= .def_1024 0.0 )))
(let ((.def_1000 (= m.speed_x__AT1 m.speed_x__AT2)))
(let ((.def_1026 (and .def_1000 .def_1025)))
(let ((.def_1031 (and .def_1026 .def_1030)))
(let ((.def_1040 (and .def_1031 .def_1039)))
(let ((.def_1041 (or .def_977 .def_1040)))
(let ((.def_1013 (= m.delta__AT1 0.0 )))
(let ((.def_1014 (and .def_975 .def_1013)))
(let ((.def_1015 (not .def_1014)))
(let ((.def_997 (= m.y__AT1 m.y__AT2)))
(let ((.def_994 (= m.x__AT2 m.x__AT1)))
(let ((.def_1008 (and .def_994 .def_997)))
(let ((.def_1009 (and .def_1000 .def_1008)))
(let ((.def_1003 (= m.speed_y__AT1 m.speed_y__AT2)))
(let ((.def_1010 (and .def_1003 .def_1009)))
(let ((.def_1016 (or .def_1010 .def_1015)))
(let ((.def_1017 (or m.EVENT.1__AT1 .def_1016)))
(let ((.def_1011 (or .def_975 .def_1010)))
(let ((.def_1012 (or m.EVENT.1__AT1 .def_1011)))
(let ((.def_1018 (and .def_1012 .def_1017)))
(let ((.def_1042 (and .def_1018 .def_1041)))
(let ((.def_982 (= m.time__AT1 m.time__AT2)))
(let ((.def_995 (and .def_982 .def_994)))
(let ((.def_998 (and .def_995 .def_997)))
(let ((.def_1001 (and .def_998 .def_1000)))
(let ((.def_1004 (and .def_1001 .def_1003)))
(let ((.def_1005 (or .def_549 .def_1004)))
(let ((.def_985 (* (- 1.0) m.time__AT2)))
(let ((.def_988 (+ m.delta__AT1 .def_985)))
(let ((.def_989 (+ m.time__AT1 .def_988)))
(let ((.def_990 (= .def_989 0.0 )))
(let ((.def_991 (or .def_977 .def_990)))
(let ((.def_992 (or m.EVENT.1__AT1 .def_991)))
(let ((.def_983 (or .def_975 .def_982)))
(let ((.def_984 (or m.EVENT.1__AT1 .def_983)))
(let ((.def_993 (and .def_984 .def_992)))
(let ((.def_1006 (and .def_993 .def_1005)))
(let ((.def_979 (= .def_977 m.event_is_timed__AT2)))
(let ((.def_976 (= m.event_is_timed__AT1 .def_975)))
(let ((.def_980 (and .def_976 .def_979)))
(let ((.def_1007 (and .def_980 .def_1006)))
(let ((.def_1043 (and .def_1007 .def_1042)))
(let ((.def_1047 (and .def_1043 .def_1046)))
(let ((.def_1048 (and .def_549 .def_1047)))
(let ((.def_1066 (and .def_1048 .def_1065)))
(let ((.def_1068 (and .def_1066 .def_1067)))
(let ((.def_929 (+ .def_926 .def_928)))
(let ((.def_932 (+ .def_930 .def_929)))
(let ((.def_957 (<= .def_932 0.0 )))
(let ((.def_965 (not .def_957)))
(let ((.def_955 (<= m.y__AT1 0.0 )))
(let ((.def_966 (or .def_955 .def_965)))
(let ((.def_561 (<= 0.0 m.y__AT1)))
(let ((.def_963 (not .def_561)))
(let ((.def_953 (<= 0.0 .def_932)))
(let ((.def_964 (or .def_953 .def_963)))
(let ((.def_967 (and .def_964 .def_966)))
(let ((.def_768 (<= m.speed_y__AT1 0.0 )))
(let ((.def_769 (not .def_768)))
(let ((.def_765 (+ .def_763 .def_762)))
(let ((.def_766 (<= .def_765 0.0 )))
(let ((.def_767 (not .def_766)))
(let ((.def_770 (or .def_767 .def_769)))
(let ((.def_771 (not .def_770)))
(let ((.def_968 (or .def_771 .def_967)))
(let ((.def_959 (not .def_953)))
(let ((.def_960 (or .def_561 .def_959)))
(let ((.def_956 (not .def_955)))
(let ((.def_958 (or .def_956 .def_957)))
(let ((.def_961 (and .def_958 .def_960)))
(let ((.def_778 (<= 0.0 .def_765)))
(let ((.def_779 (not .def_778)))
(let ((.def_776 (<= 0.0 m.speed_y__AT1)))
(let ((.def_777 (not .def_776)))
(let ((.def_780 (or .def_777 .def_779)))
(let ((.def_781 (not .def_780)))
(let ((.def_962 (or .def_781 .def_961)))
(let ((.def_969 (and .def_962 .def_968)))
(let ((.def_954 (and .def_561 .def_953)))
(let ((.def_970 (and .def_954 .def_969)))
(let ((.def_790 (and .def_766 .def_768)))
(let ((.def_787 (or .def_776 .def_779)))
(let ((.def_786 (or .def_766 .def_769)))
(let ((.def_788 (and .def_786 .def_787)))
(let ((.def_791 (and .def_788 .def_790)))
(let ((.def_785 (and .def_776 .def_778)))
(let ((.def_789 (and .def_785 .def_788)))
(let ((.def_792 (or .def_789 .def_791)))
(let ((.def_971 (and .def_792 .def_970)))
(let ((.def_933 (<= .def_932 1000.0 )))
(let ((.def_945 (not .def_933)))
(let ((.def_560 (<= m.y__AT1 100.0 )))
(let ((.def_946 (or .def_560 .def_945)))
(let ((.def_939 (<= 100.0 m.y__AT1)))
(let ((.def_943 (not .def_939)))
(let ((.def_937 (<= 1000.0 .def_932)))
(let ((.def_944 (or .def_937 .def_943)))
(let ((.def_947 (and .def_944 .def_946)))
(let ((.def_948 (or .def_771 .def_947)))
(let ((.def_938 (not .def_937)))
(let ((.def_940 (or .def_938 .def_939)))
(let ((.def_935 (not .def_560)))
(let ((.def_936 (or .def_933 .def_935)))
(let ((.def_941 (and .def_936 .def_940)))
(let ((.def_942 (or .def_781 .def_941)))
(let ((.def_949 (and .def_942 .def_948)))
(let ((.def_934 (and .def_560 .def_933)))
(let ((.def_950 (and .def_934 .def_949)))
(let ((.def_951 (and .def_792 .def_950)))
(let ((.def_604 (* (- (/ 49 10)) m.speed_y__AT1)))
(let ((.def_650 (* 3.0 .def_604)))
(let ((.def_823 (* (- 1.0) .def_650)))
(let ((.def_851 (* 2.0 .def_823)))
(let ((.def_895 (* (- 1.0) .def_851)))
(let ((.def_896 (* m.delta__AT1 .def_895)))
(let ((.def_897 (* (- 50.0) .def_896)))
(let ((.def_620 (* m.speed_x__AT1 m.speed_x__AT1)))
(let ((.def_720 (* (- 50.0) .def_620)))
(let ((.def_902 (+ .def_720 .def_897)))
(let ((.def_608 (* m.speed_y__AT1 m.speed_y__AT1)))
(let ((.def_718 (* (- 50.0) .def_608)))
(let ((.def_903 (+ .def_718 .def_902)))
(let ((.def_722 (* (- 7203.0) .def_600)))
(let ((.def_904 (+ .def_722 .def_903)))
(let ((.def_724 (* 490.0 m.y__AT1)))
(let ((.def_905 (+ .def_724 .def_904)))
(let ((.def_908 (<= 0.0 .def_905)))
(let ((.def_915 (not .def_908)))
(let ((.def_733 (* (- 5.0) .def_620)))
(let ((.def_732 (* (- 5.0) .def_608)))
(let ((.def_734 (+ .def_732 .def_733)))
(let ((.def_735 (* 49.0 m.y__AT1)))
(let ((.def_737 (+ .def_735 .def_734)))
(let ((.def_748 (<= 0.0 .def_737)))
(let ((.def_916 (or .def_748 .def_915)))
(let ((.def_906 (<= .def_905 0.0 )))
(let ((.def_738 (<= .def_737 0.0 )))
(let ((.def_739 (not .def_738)))
(let ((.def_914 (or .def_739 .def_906)))
(let ((.def_917 (and .def_914 .def_916)))
(let ((.def_918 (or .def_781 .def_917)))
(let ((.def_910 (not .def_906)))
(let ((.def_911 (or .def_738 .def_910)))
(let ((.def_749 (not .def_748)))
(let ((.def_909 (or .def_749 .def_908)))
(let ((.def_912 (and .def_909 .def_911)))
(let ((.def_913 (or .def_771 .def_912)))
(let ((.def_919 (and .def_913 .def_918)))
(let ((.def_907 (and .def_738 .def_906)))
(let ((.def_920 (and .def_907 .def_919)))
(let ((.def_921 (and .def_792 .def_920)))
(let ((.def_852 (* m.delta__AT1 .def_851)))
(let ((.def_853 (* 50.0 .def_852)))
(let ((.def_858 (+ .def_720 .def_853)))
(let ((.def_859 (+ .def_718 .def_858)))
(let ((.def_860 (+ .def_722 .def_859)))
(let ((.def_861 (+ .def_724 .def_860)))
(let ((.def_872 (<= .def_861 0.0 )))
(let ((.def_873 (not .def_872)))
(let ((.def_889 (or .def_738 .def_873)))
(let ((.def_862 (<= 0.0 .def_861)))
(let ((.def_888 (or .def_749 .def_862)))
(let ((.def_890 (and .def_888 .def_889)))
(let ((.def_891 (or .def_771 .def_890)))
(let ((.def_863 (not .def_862)))
(let ((.def_885 (or .def_748 .def_863)))
(let ((.def_884 (or .def_739 .def_872)))
(let ((.def_886 (and .def_884 .def_885)))
(let ((.def_887 (or .def_781 .def_886)))
(let ((.def_892 (and .def_887 .def_891)))
(let ((.def_883 (and .def_748 .def_862)))
(let ((.def_893 (and .def_883 .def_892)))
(let ((.def_894 (and .def_792 .def_893)))
(let ((.def_922 (or .def_894 .def_921)))
(let ((.def_661 (* 2.0 .def_620)))
(let ((.def_835 (* (- 1.0) .def_661)))
(let ((.def_836 (* m.delta__AT1 .def_835)))
(let ((.def_837 (* 25.0 .def_836)))
(let ((.def_612 (* (- (/ 49 10)) m.y__AT1)))
(let ((.def_657 (* 2.0 .def_612)))
(let ((.def_831 (* (- 1.0) .def_657)))
(let ((.def_832 (* m.delta__AT1 .def_831)))
(let ((.def_833 (* 50.0 .def_832)))
(let ((.def_842 (+ .def_833 .def_837)))
(let ((.def_653 (* 2.0 .def_608)))
(let ((.def_827 (* (- 1.0) .def_653)))
(let ((.def_828 (* m.delta__AT1 .def_827)))
(let ((.def_829 (* 25.0 .def_828)))
(let ((.def_843 (+ .def_829 .def_842)))
(let ((.def_824 (* .def_600 .def_823)))
(let ((.def_825 (* 50.0 .def_824)))
(let ((.def_844 (+ .def_825 .def_843)))
(let ((.def_624 (* m.x__AT1 m.speed_x__AT1)))
(let ((.def_669 (* (- 50.0) .def_624)))
(let ((.def_845 (+ .def_669 .def_844)))
(let ((.def_616 (* m.y__AT1 m.speed_y__AT1)))
(let ((.def_667 (* (- 50.0) .def_616)))
(let ((.def_846 (+ .def_667 .def_845)))
(let ((.def_601 (* m.delta__AT1 .def_600)))
(let ((.def_665 (* (- 2401.0) .def_601)))
(let ((.def_847 (+ .def_665 .def_846)))
(let ((.def_671 (* 1000.0 m.speed_x__AT1)))
(let ((.def_848 (+ .def_671 .def_847)))
(let ((.def_866 (<= .def_848 0.0 )))
(let ((.def_877 (not .def_866)))
(let ((.def_683 (* (- 1.0) .def_624)))
(let ((.def_682 (* (- 1.0) .def_616)))
(let ((.def_684 (+ .def_682 .def_683)))
(let ((.def_685 (* 20.0 m.speed_x__AT1)))
(let ((.def_687 (+ .def_685 .def_684)))
(let ((.def_688 (<= .def_687 0.0 )))
(let ((.def_878 (or .def_688 .def_877)))
(let ((.def_849 (<= 0.0 .def_848)))
(let ((.def_702 (<= 0.0 .def_687)))
(let ((.def_703 (not .def_702)))
(let ((.def_876 (or .def_703 .def_849)))
(let ((.def_879 (and .def_876 .def_878)))
(let ((.def_874 (or .def_739 .def_873)))
(let ((.def_875 (not .def_874)))
(let ((.def_880 (or .def_875 .def_879)))
(let ((.def_868 (not .def_849)))
(let ((.def_869 (or .def_702 .def_868)))
(let ((.def_689 (not .def_688)))
(let ((.def_867 (or .def_689 .def_866)))
(let ((.def_870 (and .def_867 .def_869)))
(let ((.def_864 (or .def_749 .def_863)))
(let ((.def_865 (not .def_864)))
(let ((.def_871 (or .def_865 .def_870)))
(let ((.def_881 (and .def_871 .def_880)))
(let ((.def_850 (and .def_702 .def_849)))
(let ((.def_882 (and .def_850 .def_881)))
(let ((.def_923 (and .def_882 .def_922)))
(let ((.def_715 (* 2.0 .def_650)))
(let ((.def_794 (* (- 1.0) .def_715)))
(let ((.def_795 (* m.delta__AT1 .def_794)))
(let ((.def_796 (* 50.0 .def_795)))
(let ((.def_801 (+ .def_720 .def_796)))
(let ((.def_802 (+ .def_718 .def_801)))
(let ((.def_803 (+ .def_722 .def_802)))
(let ((.def_804 (+ .def_724 .def_803)))
(let ((.def_807 (<= .def_804 0.0 )))
(let ((.def_814 (not .def_807)))
(let ((.def_815 (or .def_738 .def_814)))
(let ((.def_805 (<= 0.0 .def_804)))
(let ((.def_813 (or .def_749 .def_805)))
(let ((.def_816 (and .def_813 .def_815)))
(let ((.def_817 (or .def_771 .def_816)))
(let ((.def_809 (not .def_805)))
(let ((.def_810 (or .def_748 .def_809)))
(let ((.def_808 (or .def_739 .def_807)))
(let ((.def_811 (and .def_808 .def_810)))
(let ((.def_812 (or .def_781 .def_811)))
(let ((.def_818 (and .def_812 .def_817)))
(let ((.def_806 (and .def_748 .def_805)))
(let ((.def_819 (and .def_806 .def_818)))
(let ((.def_820 (and .def_792 .def_819)))
(let ((.def_716 (* m.delta__AT1 .def_715)))
(let ((.def_717 (* (- 50.0) .def_716)))
(let ((.def_726 (+ .def_720 .def_717)))
(let ((.def_727 (+ .def_718 .def_726)))
(let ((.def_728 (+ .def_722 .def_727)))
(let ((.def_729 (+ .def_724 .def_728)))
(let ((.def_746 (<= 0.0 .def_729)))
(let ((.def_747 (not .def_746)))
(let ((.def_774 (or .def_747 .def_748)))
(let ((.def_730 (<= .def_729 0.0 )))
(let ((.def_773 (or .def_730 .def_739)))
(let ((.def_775 (and .def_773 .def_774)))
(let ((.def_782 (or .def_775 .def_781)))
(let ((.def_731 (not .def_730)))
(let ((.def_760 (or .def_731 .def_738)))
(let ((.def_759 (or .def_746 .def_749)))
(let ((.def_761 (and .def_759 .def_760)))
(let ((.def_772 (or .def_761 .def_771)))
(let ((.def_783 (and .def_772 .def_782)))
(let ((.def_758 (and .def_730 .def_738)))
(let ((.def_784 (and .def_758 .def_783)))
(let ((.def_793 (and .def_784 .def_792)))
(let ((.def_821 (or .def_793 .def_820)))
(let ((.def_662 (* m.delta__AT1 .def_661)))
(let ((.def_663 (* (- 25.0) .def_662)))
(let ((.def_658 (* m.delta__AT1 .def_657)))
(let ((.def_659 (* (- 50.0) .def_658)))
(let ((.def_673 (+ .def_659 .def_663)))
(let ((.def_654 (* m.delta__AT1 .def_653)))
(let ((.def_655 (* (- 25.0) .def_654)))
(let ((.def_674 (+ .def_655 .def_673)))
(let ((.def_651 (* .def_600 .def_650)))
(let ((.def_652 (* (- 50.0) .def_651)))
(let ((.def_675 (+ .def_652 .def_674)))
(let ((.def_676 (+ .def_669 .def_675)))
(let ((.def_677 (+ .def_667 .def_676)))
(let ((.def_678 (+ .def_665 .def_677)))
(let ((.def_679 (+ .def_671 .def_678)))
(let ((.def_700 (<= 0.0 .def_679)))
(let ((.def_701 (not .def_700)))
(let ((.def_753 (or .def_701 .def_702)))
(let ((.def_680 (<= .def_679 0.0 )))
(let ((.def_752 (or .def_680 .def_689)))
(let ((.def_754 (and .def_752 .def_753)))
(let ((.def_750 (or .def_747 .def_749)))
(let ((.def_751 (not .def_750)))
(let ((.def_755 (or .def_751 .def_754)))
(let ((.def_681 (not .def_680)))
(let ((.def_743 (or .def_681 .def_688)))
(let ((.def_742 (or .def_700 .def_703)))
(let ((.def_744 (and .def_742 .def_743)))
(let ((.def_740 (or .def_731 .def_739)))
(let ((.def_741 (not .def_740)))
(let ((.def_745 (or .def_741 .def_744)))
(let ((.def_756 (and .def_745 .def_755)))
(let ((.def_714 (and .def_680 .def_688)))
(let ((.def_757 (and .def_714 .def_756)))
(let ((.def_822 (and .def_757 .def_821)))
(let ((.def_924 (or .def_822 .def_923)))
(let ((.def_628 (* (- 20.0) m.speed_x__AT1)))
(let ((.def_629 (* m.delta__AT1 .def_628)))
(let ((.def_630 (* (- 200.0) .def_629)))
(let ((.def_625 (* m.delta__AT1 .def_624)))
(let ((.def_626 (* (- 200.0) .def_625)))
(let ((.def_638 (+ .def_626 .def_630)))
(let ((.def_621 (* .def_600 .def_620)))
(let ((.def_622 (* (- 100.0) .def_621)))
(let ((.def_639 (+ .def_622 .def_638)))
(let ((.def_617 (* m.delta__AT1 .def_616)))
(let ((.def_618 (* (- 200.0) .def_617)))
(let ((.def_640 (+ .def_618 .def_639)))
(let ((.def_613 (* .def_600 .def_612)))
(let ((.def_614 (* (- 200.0) .def_613)))
(let ((.def_641 (+ .def_614 .def_640)))
(let ((.def_609 (* .def_600 .def_608)))
(let ((.def_610 (* (- 100.0) .def_609)))
(let ((.def_642 (+ .def_610 .def_641)))
(let ((.def_605 (* .def_601 .def_604)))
(let ((.def_606 (* (- 200.0) .def_605)))
(let ((.def_643 (+ .def_606 .def_642)))
(let ((.def_602 (* m.delta__AT1 .def_601)))
(let ((.def_603 (* (- 2401.0) .def_602)))
(let ((.def_644 (+ .def_603 .def_643)))
(let ((.def_593 (* m.x__AT1 m.x__AT1)))
(let ((.def_634 (* (- 100.0) .def_593)))
(let ((.def_645 (+ .def_634 .def_644)))
(let ((.def_555 (* m.y__AT1 m.y__AT1)))
(let ((.def_632 (* (- 100.0) .def_555)))
(let ((.def_646 (+ .def_632 .def_645)))
(let ((.def_636 (* 4000.0 m.x__AT1)))
(let ((.def_647 (+ .def_636 .def_646)))
(let ((.def_694 (<= 0.0 .def_647)))
(let ((.def_708 (not .def_694)))
(let ((.def_594 (* (- 1.0) .def_593)))
(let ((.def_592 (* (- 1.0) .def_555)))
(let ((.def_595 (+ .def_592 .def_594)))
(let ((.def_596 (* 40.0 m.x__AT1)))
(let ((.def_598 (+ .def_596 .def_595)))
(let ((.def_692 (<= 0.0 .def_598)))
(let ((.def_709 (or .def_692 .def_708)))
(let ((.def_599 (<= .def_598 0.0 )))
(let ((.def_706 (not .def_599)))
(let ((.def_648 (<= .def_647 0.0 )))
(let ((.def_707 (or .def_648 .def_706)))
(let ((.def_710 (and .def_707 .def_709)))
(let ((.def_704 (or .def_701 .def_703)))
(let ((.def_705 (not .def_704)))
(let ((.def_711 (or .def_705 .def_710)))
(let ((.def_696 (not .def_648)))
(let ((.def_697 (or .def_599 .def_696)))
(let ((.def_693 (not .def_692)))
(let ((.def_695 (or .def_693 .def_694)))
(let ((.def_698 (and .def_695 .def_697)))
(let ((.def_690 (or .def_681 .def_689)))
(let ((.def_691 (not .def_690)))
(let ((.def_699 (or .def_691 .def_698)))
(let ((.def_712 (and .def_699 .def_711)))
(let ((.def_649 (and .def_599 .def_648)))
(let ((.def_713 (and .def_649 .def_712)))
(let ((.def_925 (and .def_713 .def_924)))
(let ((.def_952 (and .def_925 .def_951)))
(let ((.def_972 (and .def_952 .def_971)))
(let ((.def_571 (+ m.x__AT1 .def_570)))
(let ((.def_577 (<= .def_571 0.0 )))
(let ((.def_586 (not .def_577)))
(let ((.def_575 (<= m.x__AT1 0.0 )))
(let ((.def_587 (or .def_575 .def_586)))
(let ((.def_558 (<= 0.0 m.x__AT1)))
(let ((.def_584 (not .def_558)))
(let ((.def_572 (<= 0.0 .def_571)))
(let ((.def_585 (or .def_572 .def_584)))
(let ((.def_588 (and .def_585 .def_587)))
(let ((.def_583 (<= m.speed_x__AT1 0.0 )))
(let ((.def_589 (or .def_583 .def_588)))
(let ((.def_579 (not .def_572)))
(let ((.def_580 (or .def_558 .def_579)))
(let ((.def_576 (not .def_575)))
(let ((.def_578 (or .def_576 .def_577)))
(let ((.def_581 (and .def_578 .def_580)))
(let ((.def_574 (<= 0.0 m.speed_x__AT1)))
(let ((.def_582 (or .def_574 .def_581)))
(let ((.def_590 (and .def_582 .def_589)))
(let ((.def_573 (and .def_558 .def_572)))
(let ((.def_591 (and .def_573 .def_590)))
(let ((.def_973 (and .def_591 .def_972)))
(let ((.def_566 (<= m.x__AT0 20.0 )))
(let ((.def_562 (and .def_560 .def_561)))
(let ((.def_553 (+ (- 20.0) m.x__AT1)))
(let ((.def_554 (* .def_553 .def_553)))
(let ((.def_556 (+ .def_554 .def_555)))
(let ((.def_557 (<= 400.0 .def_556)))
(let ((.def_559 (and .def_557 .def_558)))
(let ((.def_563 (and .def_559 .def_562)))
(let ((.def_552 (or .def_549 .def_551)))
(let ((.def_564 (and .def_552 .def_563)))
(let ((.def_543 (<= 0.0 m.delta__AT0)))
(let ((.def_27 (not m.EVENT.0__AT0)))
(let ((.def_25 (not m.EVENT.1__AT0)))
(let ((.def_476 (and .def_25 .def_27)))
(let ((.def_478 (not .def_476)))
(let ((.def_544 (or .def_478 .def_543)))
(let ((.def_545 (or m.EVENT.1__AT0 .def_544)))
(let ((.def_532 (* (- 10.0) m.y__AT1)))
(let ((.def_428 (* m.speed_y__AT0 m.delta__AT0)))
(let ((.def_429 (* 10.0 .def_428)))
(let ((.def_535 (+ .def_429 .def_532)))
(let ((.def_79 (* m.delta__AT0 m.delta__AT0)))
(let ((.def_427 (* (- 49.0) .def_79)))
(let ((.def_536 (+ .def_427 .def_535)))
(let ((.def_431 (* 10.0 m.y__AT0)))
(let ((.def_537 (+ .def_431 .def_536)))
(let ((.def_538 (= .def_537 0.0 )))
(let ((.def_526 (* (- 5.0) m.speed_y__AT1)))
(let ((.def_264 (* (- 49.0) m.delta__AT0)))
(let ((.def_527 (+ .def_264 .def_526)))
(let ((.def_265 (* 5.0 m.speed_y__AT0)))
(let ((.def_528 (+ .def_265 .def_527)))
(let ((.def_529 (= .def_528 0.0 )))
(let ((.def_47 (* m.speed_x__AT0 m.delta__AT0)))
(let ((.def_522 (+ .def_47 .def_521)))
(let ((.def_523 (+ m.x__AT0 .def_522)))
(let ((.def_524 (= .def_523 0.0 )))
(let ((.def_502 (= m.speed_x__AT0 m.speed_x__AT1)))
(let ((.def_525 (and .def_502 .def_524)))
(let ((.def_530 (and .def_525 .def_529)))
(let ((.def_539 (and .def_530 .def_538)))
(let ((.def_540 (or .def_478 .def_539)))
(let ((.def_515 (= m.delta__AT0 0.0 )))
(let ((.def_516 (and .def_476 .def_515)))
(let ((.def_517 (not .def_516)))
(let ((.def_499 (= m.y__AT0 m.y__AT1)))
(let ((.def_496 (= m.x__AT0 m.x__AT1)))
(let ((.def_510 (and .def_496 .def_499)))
(let ((.def_511 (and .def_502 .def_510)))
(let ((.def_505 (= m.speed_y__AT0 m.speed_y__AT1)))
(let ((.def_512 (and .def_505 .def_511)))
(let ((.def_518 (or .def_512 .def_517)))
(let ((.def_519 (or m.EVENT.1__AT0 .def_518)))
(let ((.def_513 (or .def_476 .def_512)))
(let ((.def_514 (or m.EVENT.1__AT0 .def_513)))
(let ((.def_520 (and .def_514 .def_519)))
(let ((.def_541 (and .def_520 .def_540)))
(let ((.def_483 (= m.time__AT0 m.time__AT1)))
(let ((.def_497 (and .def_483 .def_496)))
(let ((.def_500 (and .def_497 .def_499)))
(let ((.def_503 (and .def_500 .def_502)))
(let ((.def_506 (and .def_503 .def_505)))
(let ((.def_507 (or .def_25 .def_506)))
(let ((.def_486 (* (- 1.0) m.time__AT1)))
(let ((.def_489 (+ m.delta__AT0 .def_486)))
(let ((.def_490 (+ m.time__AT0 .def_489)))
(let ((.def_491 (= .def_490 0.0 )))
(let ((.def_492 (or .def_478 .def_491)))
(let ((.def_493 (or m.EVENT.1__AT0 .def_492)))
(let ((.def_484 (or .def_476 .def_483)))
(let ((.def_485 (or m.EVENT.1__AT0 .def_484)))
(let ((.def_494 (and .def_485 .def_493)))
(let ((.def_508 (and .def_494 .def_507)))
(let ((.def_480 (= .def_478 m.event_is_timed__AT1)))
(let ((.def_477 (= m.event_is_timed__AT0 .def_476)))
(let ((.def_481 (and .def_477 .def_480)))
(let ((.def_509 (and .def_481 .def_508)))
(let ((.def_542 (and .def_509 .def_541)))
(let ((.def_546 (and .def_542 .def_545)))
(let ((.def_547 (and .def_25 .def_546)))
(let ((.def_565 (and .def_547 .def_564)))
(let ((.def_567 (and .def_565 .def_566)))
(let ((.def_430 (+ .def_427 .def_429)))
(let ((.def_433 (+ .def_431 .def_430)))
(let ((.def_458 (<= .def_433 0.0 )))
(let ((.def_466 (not .def_458)))
(let ((.def_456 (<= m.y__AT0 0.0 )))
(let ((.def_467 (or .def_456 .def_466)))
(let ((.def_40 (<= 0.0 m.y__AT0)))
(let ((.def_464 (not .def_40)))
(let ((.def_454 (<= 0.0 .def_433)))
(let ((.def_465 (or .def_454 .def_464)))
(let ((.def_468 (and .def_465 .def_467)))
(let ((.def_270 (<= m.speed_y__AT0 0.0 )))
(let ((.def_271 (not .def_270)))
(let ((.def_267 (+ .def_265 .def_264)))
(let ((.def_268 (<= .def_267 0.0 )))
(let ((.def_269 (not .def_268)))
(let ((.def_272 (or .def_269 .def_271)))
(let ((.def_273 (not .def_272)))
(let ((.def_469 (or .def_273 .def_468)))
(let ((.def_460 (not .def_454)))
(let ((.def_461 (or .def_40 .def_460)))
(let ((.def_457 (not .def_456)))
(let ((.def_459 (or .def_457 .def_458)))
(let ((.def_462 (and .def_459 .def_461)))
(let ((.def_279 (<= 0.0 .def_267)))
(let ((.def_280 (not .def_279)))
(let ((.def_22 (<= 0.0 m.speed_y__AT0)))
(let ((.def_278 (not .def_22)))
(let ((.def_281 (or .def_278 .def_280)))
(let ((.def_282 (not .def_281)))
(let ((.def_463 (or .def_282 .def_462)))
(let ((.def_470 (and .def_463 .def_469)))
(let ((.def_455 (and .def_40 .def_454)))
(let ((.def_471 (and .def_455 .def_470)))
(let ((.def_291 (and .def_268 .def_270)))
(let ((.def_288 (or .def_22 .def_280)))
(let ((.def_287 (or .def_268 .def_271)))
(let ((.def_289 (and .def_287 .def_288)))
(let ((.def_292 (and .def_289 .def_291)))
(let ((.def_286 (and .def_22 .def_279)))
(let ((.def_290 (and .def_286 .def_289)))
(let ((.def_293 (or .def_290 .def_292)))
(let ((.def_472 (and .def_293 .def_471)))
(let ((.def_434 (<= .def_433 1000.0 )))
(let ((.def_446 (not .def_434)))
(let ((.def_39 (<= m.y__AT0 100.0 )))
(let ((.def_447 (or .def_39 .def_446)))
(let ((.def_440 (<= 100.0 m.y__AT0)))
(let ((.def_444 (not .def_440)))
(let ((.def_438 (<= 1000.0 .def_433)))
(let ((.def_445 (or .def_438 .def_444)))
(let ((.def_448 (and .def_445 .def_447)))
(let ((.def_449 (or .def_273 .def_448)))
(let ((.def_439 (not .def_438)))
(let ((.def_441 (or .def_439 .def_440)))
(let ((.def_436 (not .def_39)))
(let ((.def_437 (or .def_434 .def_436)))
(let ((.def_442 (and .def_437 .def_441)))
(let ((.def_443 (or .def_282 .def_442)))
(let ((.def_450 (and .def_443 .def_449)))
(let ((.def_435 (and .def_39 .def_434)))
(let ((.def_451 (and .def_435 .def_450)))
(let ((.def_452 (and .def_293 .def_451)))
(let ((.def_89 (* (- (/ 49 10)) m.speed_y__AT0)))
(let ((.def_140 (* 3.0 .def_89)))
(let ((.def_324 (* (- 1.0) .def_140)))
(let ((.def_352 (* 2.0 .def_324)))
(let ((.def_396 (* (- 1.0) .def_352)))
(let ((.def_397 (* m.delta__AT0 .def_396)))
(let ((.def_398 (* (- 50.0) .def_397)))
(let ((.def_108 (* m.speed_x__AT0 m.speed_x__AT0)))
(let ((.def_216 (* (- 50.0) .def_108)))
(let ((.def_403 (+ .def_216 .def_398)))
(let ((.def_95 (* m.speed_y__AT0 m.speed_y__AT0)))
(let ((.def_214 (* (- 50.0) .def_95)))
(let ((.def_404 (+ .def_214 .def_403)))
(let ((.def_220 (* (- 7203.0) .def_79)))
(let ((.def_405 (+ .def_220 .def_404)))
(let ((.def_223 (* 490.0 m.y__AT0)))
(let ((.def_406 (+ .def_223 .def_405)))
(let ((.def_409 (<= 0.0 .def_406)))
(let ((.def_416 (not .def_409)))
(let ((.def_234 (* (- 5.0) .def_108)))
(let ((.def_233 (* (- 5.0) .def_95)))
(let ((.def_235 (+ .def_233 .def_234)))
(let ((.def_236 (* 49.0 m.y__AT0)))
(let ((.def_238 (+ .def_236 .def_235)))
(let ((.def_249 (<= 0.0 .def_238)))
(let ((.def_417 (or .def_249 .def_416)))
(let ((.def_407 (<= .def_406 0.0 )))
(let ((.def_239 (<= .def_238 0.0 )))
(let ((.def_240 (not .def_239)))
(let ((.def_415 (or .def_240 .def_407)))
(let ((.def_418 (and .def_415 .def_417)))
(let ((.def_419 (or .def_282 .def_418)))
(let ((.def_411 (not .def_407)))
(let ((.def_412 (or .def_239 .def_411)))
(let ((.def_250 (not .def_249)))
(let ((.def_410 (or .def_250 .def_409)))
(let ((.def_413 (and .def_410 .def_412)))
(let ((.def_414 (or .def_273 .def_413)))
(let ((.def_420 (and .def_414 .def_419)))
(let ((.def_408 (and .def_239 .def_407)))
(let ((.def_421 (and .def_408 .def_420)))
(let ((.def_422 (and .def_293 .def_421)))
(let ((.def_353 (* m.delta__AT0 .def_352)))
(let ((.def_354 (* 50.0 .def_353)))
(let ((.def_359 (+ .def_216 .def_354)))
(let ((.def_360 (+ .def_214 .def_359)))
(let ((.def_361 (+ .def_220 .def_360)))
(let ((.def_362 (+ .def_223 .def_361)))
(let ((.def_373 (<= .def_362 0.0 )))
(let ((.def_374 (not .def_373)))
(let ((.def_390 (or .def_239 .def_374)))
(let ((.def_363 (<= 0.0 .def_362)))
(let ((.def_389 (or .def_250 .def_363)))
(let ((.def_391 (and .def_389 .def_390)))
(let ((.def_392 (or .def_273 .def_391)))
(let ((.def_364 (not .def_363)))
(let ((.def_386 (or .def_249 .def_364)))
(let ((.def_385 (or .def_240 .def_373)))
(let ((.def_387 (and .def_385 .def_386)))
(let ((.def_388 (or .def_282 .def_387)))
(let ((.def_393 (and .def_388 .def_392)))
(let ((.def_384 (and .def_249 .def_363)))
(let ((.def_394 (and .def_384 .def_393)))
(let ((.def_395 (and .def_293 .def_394)))
(let ((.def_423 (or .def_395 .def_422)))
(let ((.def_156 (* 2.0 .def_108)))
(let ((.def_336 (* (- 1.0) .def_156)))
(let ((.def_337 (* m.delta__AT0 .def_336)))
(let ((.def_338 (* 25.0 .def_337)))
(let ((.def_100 (* (- (/ 49 10)) m.y__AT0)))
(let ((.def_152 (* 2.0 .def_100)))
(let ((.def_332 (* (- 1.0) .def_152)))
(let ((.def_333 (* m.delta__AT0 .def_332)))
(let ((.def_334 (* 50.0 .def_333)))
(let ((.def_343 (+ .def_334 .def_338)))
(let ((.def_146 (* 2.0 .def_95)))
(let ((.def_328 (* (- 1.0) .def_146)))
(let ((.def_329 (* m.delta__AT0 .def_328)))
(let ((.def_330 (* 25.0 .def_329)))
(let ((.def_344 (+ .def_330 .def_343)))
(let ((.def_325 (* .def_79 .def_324)))
(let ((.def_326 (* 50.0 .def_325)))
(let ((.def_345 (+ .def_326 .def_344)))
(let ((.def_112 (* m.x__AT0 m.speed_x__AT0)))
(let ((.def_164 (* (- 50.0) .def_112)))
(let ((.def_346 (+ .def_164 .def_345)))
(let ((.def_104 (* m.y__AT0 m.speed_y__AT0)))
(let ((.def_162 (* (- 50.0) .def_104)))
(let ((.def_347 (+ .def_162 .def_346)))
(let ((.def_80 (* m.delta__AT0 .def_79)))
(let ((.def_160 (* (- 2401.0) .def_80)))
(let ((.def_348 (+ .def_160 .def_347)))
(let ((.def_167 (* 1000.0 m.speed_x__AT0)))
(let ((.def_349 (+ .def_167 .def_348)))
(let ((.def_367 (<= .def_349 0.0 )))
(let ((.def_378 (not .def_367)))
(let ((.def_179 (* (- 1.0) .def_112)))
(let ((.def_178 (* (- 1.0) .def_104)))
(let ((.def_180 (+ .def_178 .def_179)))
(let ((.def_181 (* 20.0 m.speed_x__AT0)))
(let ((.def_183 (+ .def_181 .def_180)))
(let ((.def_184 (<= .def_183 0.0 )))
(let ((.def_379 (or .def_184 .def_378)))
(let ((.def_350 (<= 0.0 .def_349)))
(let ((.def_198 (<= 0.0 .def_183)))
(let ((.def_199 (not .def_198)))
(let ((.def_377 (or .def_199 .def_350)))
(let ((.def_380 (and .def_377 .def_379)))
(let ((.def_375 (or .def_240 .def_374)))
(let ((.def_376 (not .def_375)))
(let ((.def_381 (or .def_376 .def_380)))
(let ((.def_369 (not .def_350)))
(let ((.def_370 (or .def_198 .def_369)))
(let ((.def_185 (not .def_184)))
(let ((.def_368 (or .def_185 .def_367)))
(let ((.def_371 (and .def_368 .def_370)))
(let ((.def_365 (or .def_250 .def_364)))
(let ((.def_366 (not .def_365)))
(let ((.def_372 (or .def_366 .def_371)))
(let ((.def_382 (and .def_372 .def_381)))
(let ((.def_351 (and .def_198 .def_350)))
(let ((.def_383 (and .def_351 .def_382)))
(let ((.def_424 (and .def_383 .def_423)))
(let ((.def_211 (* 2.0 .def_140)))
(let ((.def_295 (* (- 1.0) .def_211)))
(let ((.def_296 (* m.delta__AT0 .def_295)))
(let ((.def_297 (* 50.0 .def_296)))
(let ((.def_302 (+ .def_216 .def_297)))
(let ((.def_303 (+ .def_214 .def_302)))
(let ((.def_304 (+ .def_220 .def_303)))
(let ((.def_305 (+ .def_223 .def_304)))
(let ((.def_308 (<= .def_305 0.0 )))
(let ((.def_315 (not .def_308)))
(let ((.def_316 (or .def_239 .def_315)))
(let ((.def_306 (<= 0.0 .def_305)))
(let ((.def_314 (or .def_250 .def_306)))
(let ((.def_317 (and .def_314 .def_316)))
(let ((.def_318 (or .def_273 .def_317)))
(let ((.def_310 (not .def_306)))
(let ((.def_311 (or .def_249 .def_310)))
(let ((.def_309 (or .def_240 .def_308)))
(let ((.def_312 (and .def_309 .def_311)))
(let ((.def_313 (or .def_282 .def_312)))
(let ((.def_319 (and .def_313 .def_318)))
(let ((.def_307 (and .def_249 .def_306)))
(let ((.def_320 (and .def_307 .def_319)))
(let ((.def_321 (and .def_293 .def_320)))
(let ((.def_212 (* m.delta__AT0 .def_211)))
(let ((.def_213 (* (- 50.0) .def_212)))
(let ((.def_225 (+ .def_216 .def_213)))
(let ((.def_226 (+ .def_214 .def_225)))
(let ((.def_227 (+ .def_220 .def_226)))
(let ((.def_228 (+ .def_223 .def_227)))
(let ((.def_247 (<= 0.0 .def_228)))
(let ((.def_248 (not .def_247)))
(let ((.def_276 (or .def_248 .def_249)))
(let ((.def_229 (<= .def_228 0.0 )))
(let ((.def_275 (or .def_229 .def_240)))
(let ((.def_277 (and .def_275 .def_276)))
(let ((.def_283 (or .def_277 .def_282)))
(let ((.def_230 (not .def_229)))
(let ((.def_261 (or .def_230 .def_239)))
(let ((.def_260 (or .def_247 .def_250)))
(let ((.def_262 (and .def_260 .def_261)))
(let ((.def_274 (or .def_262 .def_273)))
(let ((.def_284 (and .def_274 .def_283)))
(let ((.def_259 (and .def_229 .def_239)))
(let ((.def_285 (and .def_259 .def_284)))
(let ((.def_294 (and .def_285 .def_293)))
(let ((.def_322 (or .def_294 .def_321)))
(let ((.def_157 (* m.delta__AT0 .def_156)))
(let ((.def_158 (* (- 25.0) .def_157)))
(let ((.def_153 (* m.delta__AT0 .def_152)))
(let ((.def_154 (* (- 50.0) .def_153)))
(let ((.def_169 (+ .def_154 .def_158)))
(let ((.def_147 (* m.delta__AT0 .def_146)))
(let ((.def_150 (* (- 25.0) .def_147)))
(let ((.def_170 (+ .def_150 .def_169)))
(let ((.def_141 (* .def_79 .def_140)))
(let ((.def_144 (* (- 50.0) .def_141)))
(let ((.def_171 (+ .def_144 .def_170)))
(let ((.def_172 (+ .def_164 .def_171)))
(let ((.def_173 (+ .def_162 .def_172)))
(let ((.def_174 (+ .def_160 .def_173)))
(let ((.def_175 (+ .def_167 .def_174)))
(let ((.def_196 (<= 0.0 .def_175)))
(let ((.def_197 (not .def_196)))
(let ((.def_254 (or .def_197 .def_198)))
(let ((.def_176 (<= .def_175 0.0 )))
(let ((.def_253 (or .def_176 .def_185)))
(let ((.def_255 (and .def_253 .def_254)))
(let ((.def_251 (or .def_248 .def_250)))
(let ((.def_252 (not .def_251)))
(let ((.def_256 (or .def_252 .def_255)))
(let ((.def_177 (not .def_176)))
(let ((.def_244 (or .def_177 .def_184)))
(let ((.def_243 (or .def_196 .def_199)))
(let ((.def_245 (and .def_243 .def_244)))
(let ((.def_241 (or .def_230 .def_240)))
(let ((.def_242 (not .def_241)))
(let ((.def_246 (or .def_242 .def_245)))
(let ((.def_257 (and .def_246 .def_256)))
(let ((.def_210 (and .def_176 .def_184)))
(let ((.def_258 (and .def_210 .def_257)))
(let ((.def_323 (and .def_258 .def_322)))
(let ((.def_425 (or .def_323 .def_424)))
(let ((.def_116 (* (- 20.0) m.speed_x__AT0)))
(let ((.def_117 (* m.delta__AT0 .def_116)))
(let ((.def_118 (* (- 200.0) .def_117)))
(let ((.def_113 (* m.delta__AT0 .def_112)))
(let ((.def_114 (* (- 200.0) .def_113)))
(let ((.def_127 (+ .def_114 .def_118)))
(let ((.def_109 (* .def_79 .def_108)))
(let ((.def_110 (* (- 100.0) .def_109)))
(let ((.def_128 (+ .def_110 .def_127)))
(let ((.def_105 (* m.delta__AT0 .def_104)))
(let ((.def_106 (* (- 200.0) .def_105)))
(let ((.def_129 (+ .def_106 .def_128)))
(let ((.def_101 (* .def_79 .def_100)))
(let ((.def_102 (* (- 200.0) .def_101)))
(let ((.def_130 (+ .def_102 .def_129)))
(let ((.def_96 (* .def_79 .def_95)))
(let ((.def_98 (* (- 100.0) .def_96)))
(let ((.def_131 (+ .def_98 .def_130)))
(let ((.def_90 (* .def_80 .def_89)))
(let ((.def_93 (* (- 200.0) .def_90)))
(let ((.def_132 (+ .def_93 .def_131)))
(let ((.def_81 (* m.delta__AT0 .def_80)))
(let ((.def_84 (* (- 2401.0) .def_81)))
(let ((.def_133 (+ .def_84 .def_132)))
(let ((.def_71 (* m.x__AT0 m.x__AT0)))
(let ((.def_122 (* (- 100.0) .def_71)))
(let ((.def_134 (+ .def_122 .def_133)))
(let ((.def_32 (* m.y__AT0 m.y__AT0)))
(let ((.def_120 (* (- 100.0) .def_32)))
(let ((.def_135 (+ .def_120 .def_134)))
(let ((.def_125 (* 4000.0 m.x__AT0)))
(let ((.def_136 (+ .def_125 .def_135)))
(let ((.def_190 (<= 0.0 .def_136)))
(let ((.def_204 (not .def_190)))
(let ((.def_72 (* (- 1.0) .def_71)))
(let ((.def_70 (* (- 1.0) .def_32)))
(let ((.def_73 (+ .def_70 .def_72)))
(let ((.def_75 (* 40.0 m.x__AT0)))
(let ((.def_77 (+ .def_75 .def_73)))
(let ((.def_188 (<= 0.0 .def_77)))
(let ((.def_205 (or .def_188 .def_204)))
(let ((.def_78 (<= .def_77 0.0 )))
(let ((.def_202 (not .def_78)))
(let ((.def_137 (<= .def_136 0.0 )))
(let ((.def_203 (or .def_137 .def_202)))
(let ((.def_206 (and .def_203 .def_205)))
(let ((.def_200 (or .def_197 .def_199)))
(let ((.def_201 (not .def_200)))
(let ((.def_207 (or .def_201 .def_206)))
(let ((.def_192 (not .def_137)))
(let ((.def_193 (or .def_78 .def_192)))
(let ((.def_189 (not .def_188)))
(let ((.def_191 (or .def_189 .def_190)))
(let ((.def_194 (and .def_191 .def_193)))
(let ((.def_186 (or .def_177 .def_185)))
(let ((.def_187 (not .def_186)))
(let ((.def_195 (or .def_187 .def_194)))
(let ((.def_208 (and .def_195 .def_207)))
(let ((.def_138 (and .def_78 .def_137)))
(let ((.def_209 (and .def_138 .def_208)))
(let ((.def_426 (and .def_209 .def_425)))
(let ((.def_453 (and .def_426 .def_452)))
(let ((.def_473 (and .def_453 .def_472)))
(let ((.def_48 (+ m.x__AT0 .def_47)))
(let ((.def_53 (<= .def_48 0.0 )))
(let ((.def_62 (not .def_53)))
(let ((.def_51 (<= m.x__AT0 0.0 )))
(let ((.def_63 (or .def_51 .def_62)))
(let ((.def_36 (<= 0.0 m.x__AT0)))
(let ((.def_60 (not .def_36)))
(let ((.def_49 (<= 0.0 .def_48)))
(let ((.def_61 (or .def_49 .def_60)))
(let ((.def_64 (and .def_61 .def_63)))
(let ((.def_59 (<= m.speed_x__AT0 0.0 )))
(let ((.def_65 (or .def_59 .def_64)))
(let ((.def_55 (not .def_49)))
(let ((.def_56 (or .def_36 .def_55)))
(let ((.def_52 (not .def_51)))
(let ((.def_54 (or .def_52 .def_53)))
(let ((.def_57 (and .def_54 .def_56)))
(let ((.def_19 (<= 0.0 m.speed_x__AT0)))
(let ((.def_58 (or .def_19 .def_57)))
(let ((.def_66 (and .def_58 .def_65)))
(let ((.def_50 (and .def_36 .def_49)))
(let ((.def_67 (and .def_50 .def_66)))
(let ((.def_474 (and .def_67 .def_473)))
(let ((.def_41 (and .def_39 .def_40)))
(let ((.def_30 (+ m.x__AT0 (- 20.0) )))
(let ((.def_31 (* .def_30 .def_30)))
(let ((.def_33 (+ .def_31 .def_32)))
(let ((.def_35 (<= 400.0 .def_33)))
(let ((.def_37 (and .def_35 .def_36)))
(let ((.def_42 (and .def_37 .def_41)))
(let ((.def_28 (or .def_25 .def_27)))
(let ((.def_43 (and .def_28 .def_42)))
(let ((.def_16 (= m.y__AT0 0.0 )))
(let ((.def_13 (= m.x__AT0 0.0 )))
(let ((.def_9 (= m.time__AT0 0.0 )))
(let ((.def_11 (and .def_9 m.event_is_timed__AT0)))
(let ((.def_14 (and .def_11 .def_13)))
(let ((.def_17 (and .def_14 .def_16)))
(let ((.def_20 (and .def_17 .def_19)))
(let ((.def_23 (and .def_20 .def_22)))
(let ((.def_44 (and .def_23 .def_43)))
(let ((.def_5 (<= m.x__AT2 20.0 )))
(let ((.def_6 (not .def_5)))
(let ((.def_45 (and .def_6 .def_44)))
(let ((.def_475 (and .def_45 .def_474)))
(let ((.def_568 (and .def_475 .def_567)))
(let ((.def_974 (and .def_568 .def_973)))
(let ((.def_1069 (and .def_974 .def_1068)))
(let ((.def_1475 (and .def_1069 .def_1474)))
.def_1475))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
